Section: New Results

Security protocols

Analysis of equivalence properties

Participants : Vincent Cheval, Véronique Cortier, Antoine Dallon, Ivan Gazeau, Steve Kremer, Joseph Lallemand, Itsaka Rakotonirina, Christophe Ringeissen.

Automatic tools based on symbolic models have been successful in analyzing security protocols. These tools are particularly well adapted for trace properties (e.g. secrecy or authentication). A wide range of security properties, such as anonymity properties in electronic voting and auctions, unlinkability in RFID protocols and mobile phone protocols, are however naturally expressed in terms of indistinguishability, which is not a trace property. Indistinguishability is naturally formalized as an observational or trace equivalence in cryptographic process calculi, such as the applied pi calculus. While several decision procedures have already been proposed for verifying equivalence properties the resulting tools are often rather limited, and lack efficiency.

Our results are centered around the development of several, complementary verification tools for verifying equivalence properties. These tools are complementary in terms of expressivity, precision and efficiency.

• The Akiss tool provides good expressivity as it supports a large number of cryptographic primitives (including the XOR primitive, extremely popular in low energy devices such as RFID tags) and protocols with else branches. It allows verification for a bounded number of protocol sessions. The tool is precise for a class of determinate processes, and can approximate equivalence for other protocols. The tool however suffers from efficiency problems when the number of sessions increases. The computation can be partially distributed on different cores. To overcome these efficiency problems of the Akiss tool, Gazeau and Kremer completely revisit the theory underlying Akiss. Rather than enumerating the possible traces, the new version directly reasons about partial ordered traces. A new implementation is also in progress and the first results seem extremely promising.

• The SAT-Equiv tool is based on a novel algorithm, based on graph planning and SAT-solving. The tool has a limited expressivity in that it allows only the most standard cryptographic primitives, requires protocols to be determinate and does not support protocols with else branches. The tool is however extremely efficient, allowing verification for a very large (but bounded) number of sessions (where most other tools have to stop after one or two sessions). Cortier and Dallon, in collaboration with Delaune (IRISA), have presented at ESORICS'18 [20] an extension of SAT-EQUIV to support protocols with phases and a large class of cryptographic primitives that encompasses standard primitives. This required to first show a small attack property: whenever two protocols are not in equivalence, there exists a well-typed witness of non equivalence. This result was initially proved for symmetric encryption only and now holds for a large class of primitives [37].

• The DEEPSEC tool, presented by Cheval, Kremer and Rakotonirina at S&P'18 [18], is a new tool that allows for user-defined cryptographic primitives that can be modelled as a subterm convergent rewrite system (slightly more restricted than AKISS), but supports the whole applied pi calculus, except for bounding the number of sessions. It is precise, in that it decides equivalence (without any approximations) and has good efficiency (slightly less than SAT-Equiv) for the class of determinate processes (where partial order reductions apply). Their work also settled the question of the exact complexity of deciding different equivalences - static equivalence, trace equivalence and bisimulation. In particular they were able to show that both deciding trace equivalence and bisimulation in the case of cryptographic primitives modelled by subterm convergent rewrite systems are co-NEXP complete problems – this is a strong, new insight, solving a longstanding open question about the complexity of this problem. The DEEPSEC tool also implements state of the art partial order reductions and the verification can be distributed on different cores on a single machine and also on clusters of machines, as detailed in a CAV'18 tool paper [19].

• Unlike the above tools, the TYPE-EQ tool supports verification of both a bounded and unbounded number of protocol sessions (and a mix of them). It is based on a novel approach for equivalence properties. Instead of deciding equivalence like for the previous approaches, the tool uses a type system which is sound w.r.t. equivalence. Regarding precision, the tool is not complete, i.e. it may provide false attacks. It induces a significant speedup compared to previous tools for a bounded number of sessions and compares similarly to ProVerif  [47] for an unbounded number of sessions. In collaboration with Maffei and Grimm, Lallemand and Cortier [23] extend this approach to all standard primitives and improve its precision, allowing to branch on secrets.

From a more foundational point of view, Ringeissen, in collaboration with Erbatur (LMU, Germany) and Marshall (Univ Mary Washington, USA), study decision procedures for two knowledge problems critical to the verification of security protocols, namely the intruder deduction and the static equivalence problems. These problems can be related to particular forms of context matching and context unification. Both problems are defined with respect to an equational theory and are known to be decidable when the equational theory is given by a subterm convergent term rewrite system. In a paper presented at UNIF'18 [33] they investigate the case of a subterm convergent equational term rewrite system defined modulo an equational theory, like Commutativity or Associativity-Commutativity. They show that for certain classes of such equational theories, namely the shallow classes, the two knowledge problems remain decidable.

Verification of protocols with global states

Participants : Vincent Cheval, Véronique Cortier, Jannik Dreier, Mathieu Turuani.

One known challenge when analysing security protocols for an unbounded number of sessions is the case of protocols with global states such as counters, tables, or more generally, memory cells. The popular tool ProVerif  [47] fails to analyse such protocols, due to its internal abstraction. Cheval, Cortier, and Turuani have devised a generic transformation of the security properties queried to ProVerif. In a paper presented at CSF'18 [17], they proved the soundness of the transformation and implement it into a front-end GSVerif. Their experiments show that GSVerif (combined with ProVerif) outperforms the few existing tools, both in terms of efficiency and protocol coverage. GSVerif was successfully applied to a dozen of protocols of the literature, yielding the first fully automatic proof of a security API and a payment protocol of the literature.

The TAMARIN prover is a state-of-the-art verification tool for cryptographic protocols in the symbolic model. Dreier, in collaboration with Hirschi, Sasse (ETH Zurich), and Radomirovic (Dundee), improved the underlying theory and the tool to deal with an equational theory modeling XOR operations. Exclusive-or (XOR) operations are common in cryptographic protocols, in particular in RFID protocols and electronic payment protocols. Although there are numerous applications, due to the inherent complexity of faithful models of XOR, there is only limited tool support for the verification of cryptographic protocols using XOR. This makes TAMARIN the first tool to support simultaneously this large set of equational theories, protocols with global mutable state, an unbounded number of sessions, and complex security properties including observational equivalence. We demonstrated the effectiveness of our approach by analyzing several protocols that rely on XOR, in particular multiple RFID-protocols, where we can identify attacks as well as provide proofs. These results were presented at CSF'18 [29].

Analysis of deployed protocols

Participants : Jannik Dreier, Charlie Jacomme, Steve Kremer.

Multi-factor authentication.

Passwords are still the most widespread means for authenticating users, even though they have been shown to create huge security problems. This motivated the use of additional authentication mechanisms used in so-called multi-factor authentication protocols. In a paper, published at CSF'18 [30] Jacomme and Kremer define a detailed threat model for this kind of protocols: while in classical protocol analysis attackers control the communication network, the idea is to take into account that many communications are performed over TLS channels, that computers may be infected by different kinds of malwares, that attackers could perform phishing, and that humans may omit some actions. This model has been formalized in the applied pi calculus and perform an extensive analysis and comparison of several widely used protocols — variants of Google 2 step and FIDO U2F. The analysis is completely automated, generating systematically all combinations of threat scenarios for each of the protocols and using the ProVerif tool  [47] for automated protocol analysis. Even though threat scenarios are eliminated as soon as results are implied by weaker scenarios, the analysis required over 6 000 calls to ProVerif, yet finishes in only a few minutes. Their analysis highlights weaknesses and strengths of the different protocols, and allows them to suggest several small modifications of the existing protocols which are easy to implement, yet improve their security in several threat scenarios.

5G Authentication.

Mobile communication networks connect much of the world's population. The security of users' calls, SMSs, and mobile data depends on the guarantees provided by the Authenticated Key Exchange protocols used. For the next-generation network (5G), the 3GPP group has standardized the 5G AKA protocol for this purpose. We provided the first comprehensive formal model of a protocol from the AKA family: 5G AKA. We also extracted precise requirements from the 3GPP standards defining 5G and we identified missing security goals. Using the security protocol verification tool Tamarin and its recent extension to support XOR, we conducted a full, systematic, security evaluation of the model with respect to the 5G security goals. Our automated analysis identifies the minimal security assumptions required for each security goal and we found that some critical security goals are not met, except under additional assumptions missing from the standard. Finally, we made explicit recommendations with provably secure fixes for the attacks and weaknesses we found. These results were presented at CCS'18 [13].

Authentication Methods with PIN Codes.

Touch screens have become ubiquitous in the past few years, like for instance in smartphones and tablets. These devices are often the entry door to numerous information systems, hence having a secure and practical authentication mechanism is crucial. In this work, we examined the complexity of different authentication methods specifically designed for such devices. We studied the common technology to authenticate a user using a Personal Identifier Number code (PIN code). Entering the code is a critical moment where there are several possibilities for an attacker to discover the secret. We considered three attack models: a Bruteforce Attack (BA) model, a Smudge Attack (SA) model, and an Observation Attack (OA) model where the attacker sees the user logging in on his device. The aim of the intruder is to learn the secret code. Our goal is to propose alternative methods to enter a PIN code. We compared such different methods in terms of security. Some methods require more intentional resources than other, this is why we performed a psychological study on the different methods to evaluate the users' perception of the different methods and their usage. This work was presented at RCIS'18 [16].

Protocol design

Participant : Jannik Dreier.

A Cryptographer's Conspiracy Santa.

In Conspiracy Santa, a variant of Secret Santa, a group of people offer each other Christmas gifts, where each member of the group receives a gift from the other members of the group. To that end, the members of the group form conspiracies, to decide on appropriate gifts, and usually divide the cost of the gift among all participants of the conspiracy. This requires to settle the shared expenses per conspiracy, so Conspiracy Santa can actually be seen as an aggregation of several shared expenses problems. In this work, we showed that the problem of finding a minimal number of transactions when settling shared expenses is NP-complete. Still, there exists good greedy approximations. Second, we presented a greedy distributed secure solution to Conspiracy Santa. This solution allows a group of people to share the expenses for the gifts in such a way that no participant will learn the price of his/her gift, but at the same time notably reduces the number of transactions with respect to a naive aggregation. Furthermore, our solution does not require a trusted third party, and can either be implemented physically (the participants are in the same room and exchange money) or, virtually, using a cryptocurrency. This work was presented at FUN'18 [14].

A Physical Zero-Knowledge Proof for Makaro.

Makaro is a logic game similar to Sudoku. In Makaro, a grid has to be filled with numbers such that: given areas contain all the numbers up to the number of cells in the area, no adjacent numbers are equal, and some cells provide restrictions on the largest adjacent number. In this work we proposed a proven secure physical algorithm, only relying on cards, to realize a zero-knowledge proof of knowledge for Makaro. It allows a player to show that he/she knows a solution without revealing it. This work was presented at SSS'18 [15].